In this paper, we propose an unbounded model checking method for feature interaction verification for telecommunication systems. Unbounded model checking is a SAT-based verification method and has attracted recent attention as a powerful approach. The interpolation-based approach is one of the most promising unbounded model checking methods and has been proven to be effective for hardware verification. However, the application of unbounded model checking to asynchronous systems, such as telecommunication systems, has rarely been practiced. This is because, with the conventional encoding, the behavior of an asynchronous system can only be represented as a large propositional formula, thus resulting in large computational cost. To overcome this problem we propose to use a new scheme for encoding the behavior of the system and adapt the unbounded model checking algorithm to this encoding. By exploiting the concurrency of an asynchronous system, this encoding scheme allows a very concise formula to represent system's behavior. To demonstrate the effectiveness of our approach, we conduct experiments where 21 pairs of telecommunication services are verified using several methods including ours. The results show that our approach exhibits significant speed-up over unbounded model checking using the traditional encoding.

We propose a lightweight scheme for fault diagnosis in time-triggered (TT) systems. An existing scheme is preferable in its capability but incurs computation time that can be prohibitively large for some real-time systems, such as automotive control systems. Our proposed scheme, which we call voting sharing, can substantially reduce the computation time by sharing the diagnosis result obtained by each node with all nodes in the system. We clarify the properties of the voting sharing scheme with respect to fault tolerance and show some experimental results.

A Peer-To-Peer (P2P) application uses an overlay network which is a virtual network constructed over the physical network. Traditional overlay construction methods do not take physical location of nodes into consideration, resulting in a large amount of redundant traffic. Some proximity-aware construction methods have been proposed to address this problem. These methods typically connect nearby nodes in the physical network. However, as the number of nodes increases, the path length of a route between two distant nodes rapidly increases. To alleviate this problem, we propose a technique which can be incorporated in existing overlay construction methods. The idea behind this technique is to employ long links to directly connect distant nodes. Through simulation experiments, we show that using our proposed technique, networks can achieve small path length and low communication cost while maintaining high resiliency to failures.

This letter discusses the applicability of boolean satisfiability (SAT) solving to pairwise testing in practice. Due to its recent rapid advance, using SAT solving seems a promising approach for search-based testing and indeed has already been practiced in test generation for pairwise testing. The previous approaches use SAT solving either for finding a small test set in the absence of parameter constraints or handling constraints, but not for both. This letter proposes an approach that uses a SAT solver for constructing a test set for pairwise testing in the presence of parameter constraints. This allows us to make full use of SAT solving for pairwise testing in practice.